(tt = ff  ) 

latex

ProofTree

Definitions	, t  T, P  Q, A, False, x:A. B(x), if b then t else f fi , ff, tt
Lemmas	bfalse wf, btrue wf, bool wf, ifthenelse wf